1. Field of the Invention
The present disclosure relates to the verification of digital circuits. In particular, the present disclosure relates to a method and a system for determining the progress and/or the quality of a formal verification process of digital circuit designs.
2. Background and Related Art
Digital circuits such as processors or application specific integrated circuits (ASICS) have become increasingly complex over the last decades. Engineers developing, designing and testing digital circuits have to ensure that a digital circuit has the required functionality and that bugs or malfunctions are excluded as far as possible. The design of a digital circuit should thus be verified before the actual production starts to avoid costs for erroneous circuits having undetected bugs. Simulation of a digital circuit design was therefore frequently applied in order to simulate the function of a digital circuit design. Computing a simulation can be time consuming and expensive with modern complex designs.
Formal verification of digital circuits has become an alternative or complementary tool to simulation of digital circuits. Verification of a digital circuit is usually performed during the design of a digital circuit to verify that the planned design provides the desired functionality without relevant bugs. Formal verification uses formal assertions or formal properties which describe aspects of behaviour of the digital circuit design. A set of the formal assertions or formal properties is used to describe the behaviour of functions of the digital circuit. The digital circuit is then verified by formally verifying that each one of the formal properties holds for the description of the digital circuit design.
In many cases a design is described at the register transfer level (RTL) using languages such as VHDL, Verilog, SystemVerilog, C, C++, System C or others.
It is important to know whether a design has been completely verified or has been verified to an extent that verification can be considered sufficiently complete and safe.
State of the art literature determines the coverage of a verification process by determining whether enough assertions or properties have been established to cover the entire behaviour of the design. A summary of the known methods is given in the article “Coverage Metrics for Formal Verification” by H. Chockler et al. Proceedings of CHARME, 2003
European Patent EP 1 764 715, also published as US 2007/0226663 describes a method for the determination of the quality of a set of formal properties used in formal verification.
U.S. Pat. No. 6,484,134 discloses a method for determining the property coverage. This method determines which functions of a digital circuit are actually covered by the properties.
All of the above prior art relates to the problem of property coverage, i.e. to the questions whether the formal properties used in formal verification are sufficient to describe the complete behaviour of the digital circuit under verification. While there is a wide state of the art relating to the formal properties or assertions, there is no reliable method or system for determining the progress of a verification process on the description of a digital circuit design.
U.S. Pat. No. 6,594,804 describes a system to provide static coverage analysis. This disclosure teaches a system that determines what portions of a circuit design can and cannot be verified using a given set of properties. This method relates to a signal coverage and tries to identify uncovered signals. A signal is determined uncovered if a change in the gate driving the signal does not change the outcome of verification. In the case of U.S. Pat. No. 6,594,804 either ‘0’ or ‘1’ is input and the propagation of the signal synthesised hardware description of a design.
The proposed method can only be applied to a synthesised hardware design and cannot be applied to a RTL description. In other words the method of U.S. Pat. No. 6,594,804 can only be applied at a later stage of the design and cannot be used at the RTL level. Furthermore, it is necessary to repeat the analysis for each individual fault independently, which requires considerable computing resources time and costs.
It is an object of the present invention to overcome the disadvantages of prior art. It is another object of the present disclosure to provide a method, a system and a computer program product for determining the status of a formal verification process of a design under verification.